shaken
뭐ut dennistic
antwort
Hat sich der dritte in Bunde abgemeldet?
Nein!
So, wir haben heute woanders...
Er hat gar nicht so richtig gesagt wo eigentlich.
Entschuldigung.
Ja, für die letztes Mal abwesenden wiederhole ich einfach nochmal.
Ich höre einfach zu.
Also, was wir uns gerade angucken ist die sogenannte Hennessey-Mürner-Logik.
Das ist also eine Logik mit Formeln, die ich auswerte in Zuständen eines LTS.
Schreibe mal die Grammatik der Formeln hin.
Also jetzt den nächsten Mal die üblichen ruhigen Zutaten.
Also Spalsum, nicht und und.
Und als Besonderheit eben diesen Modal-Operator.
Jetzt sieht er anders aus.
Letztes Mal war es eine Box mit einem kleinen A.
Nein, das ist ein Ecker.
So.
Ach so, nicht A sondern ein A.
Ja.
Wobei also diese Boxen indiziert sind über alle Aktionen.
Und man definiert dann die Semantik von dem Ding, in dem man sagt, wir geben so ein Transitionssystem T.
Habe ich das in der Nächste geschrieben oder mit davor?
Ich muss nachgucken.
Ich habe mir alles da.
Da stand einfach nur sein T ist gleich Klammeraufbuhl etc. LTS.
Dann hatten wir ein T,S.
T,S genau.
Also T,S erfüllt Phi.
Das ist also das, was wir als Semantik von dem Ding sehen.
Also wir sagen, in welche Zustände, in welchen LTS erfüllen jetzt so eine Formel.
Und das ist also wie immer dekursiv definiert über eine Serie von Klauseln, eine für die Eintracht in der Grammatik.
Also Bottom wird halt nicht erfüllt.
Nicht Phi wird erfüllt genau dann, wenn Phi eben nicht erfüllt wird.
Eine Konjunktion wird erfüllt, wenn der erste Anteil erfüllt wird.
Und der zweite Anteil erfüllt wird.
Das war jetzt der langweilige Teil.
Der eigentliche Ritz an der Sache ist das mit der Box.
Also T,S erfüllt Box A Phi.
Genau, wenn.
Also gemeint ist immer Alpha.
Das kann insbesondere auch ein Tau sein.
Das sind aber sämtliche Aktionen, die wir jetzt belassen.
So.
Also T,S erfüllt Box Alpha Phi.
Genau dann, wenn.
Für alle, also die Box ist ein verkapselter Alkantur.
Also dramatikalisch habe ich jetzt ein Problem.
Presenters
Zugänglich über
Offener Zugang
Dauer
01:19:00 Min
Aufnahmedatum
2014-06-17
Hochgeladen am
2019-04-21 06:59:03
Sprache
de-DE
-
erläutern semantische Grundbegriffe, insbesondere Systemtypen und Systemäquivalenzen, und identifizieren ihre wesentlichen Eigenschaften
-
erläutern die Syntax und Semantik von Logiken und Prozesskalkülen
-
fassen wesentliche Metaeigenschaften von Logiken und Prozesskalkülen zusammen.
-
übersetzen Prozessalgebraische Terme in ihre denotationelle und operationelle Semantik
-
prüfen Systeme auf verschiedene Formen von Bsimilarität
-
prüfen Erfüllheit modaler Fixpunktformeln in gegebenen Systemen
-
implementieren nebenläufige Probleme in Prozessalgebren
-
spezifizieren das Verhalten nebenläufiger Prozesse im modalen mu-Kalkül.
-
leiten einfache Meta-Eigenschaften von Kalkülen her
-
wählen für die Läsung gegebener nebenläufiger Probleme geeignete Formalismen aus
-
vergleichen prozessalgebraische und logische Kalküle hinsichtlich Ausdrucksmächtigkeit und Berechenbarkeitseigenschaften
-
hinterfragen die Eignung eines Kalküls zur Lösung einer gegebenen Problemstellung
Literatur:
- Robin Milner, Communication and Concurrency, Prentice-Hall, 1989
-
Julian Bradfield and Colin Stirling, Modal mu-calculi. In: Patrick Blackburn, Johan van Benthem and Frank Wolter (eds.), The Handbook of Modal Logic, pp. 721-756. Elsevier, 2006.
-
Jan Bergstra, Alban Ponse and Scott Smolka (eds.), Handbook of Process Algebra, Elsevier, 2006.